Nuprl Lemma : l_disjoint_nil
11,40
postcript
pdf
A
:Type,
L
:(
A
List). l_disjoint(
A
;[];
L
)
latex
Definitions
Void
,
(
x
l
)
,
x
:
A
B
(
x
)
,
P
&
Q
,
x
:
A
B
(
x
)
,
P
Q
,
False
,
A
,
Type
,
type
List
,
t
T
,
s
=
t
,
,
A
c
B
,
a
<
b
,
P
Q
,
P
Q
,
x
:
A
.
B
(
x
)
,
l_disjoint(
T
;
l1
;
l2
)
Lemmas
not
functionality
wrt
iff
,
and
functionality
wrt
iff
,
nil
member
origin
A:Type, L:(A List). l_disjoint(A;[];L) A:Type, L:(A List). l_disjoint(A;[];L) 
l)
B(x)
B(x)
Q
A T
B
Q Qx:A. B(x)